/*
 * Alloy Analyzer
 * Copyright (c) 2002 Massachusetts Institute of Technology
 *
 * The Alloy Analyzer is free software; you can redistribute it and/or modify
 * it under the terms of the GNU General Public License as published by
 * the Free Software Foundation; either version 2 of the License, or
 * (at your option) any later version.
 *
 * The Alloy Analyzer is distributed in the hope that it will be useful,
 * but WITHOUT ANY WARRANTY; without even the implied warranty of
 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
 * GNU General Public License for more details.
 *
 * You should have received a copy of the GNU General Public License
 * along with the Alloy Analyzer; if not, write to the Free Software
 * Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA  02111-1307  USA
 */

package alloy.ast;

import java.util.ArrayList;
import java.util.Collection;
import java.util.Collections;
import java.util.HashMap;
import java.util.Iterator;
import java.util.List;
import java.util.Map;
import java.util.Set;

import alloy.semantic.AlreadyMappedException;
import alloy.semantic.ExprTypeCheckVisitor;
import alloy.semantic.SignatureReferenceCounter;
import alloy.util.Dbg;
import alloy.util.Msg;

/**
   Information about a {@link Module}.  Includes information about visible paragraph
   names, including whether a name must be fully qualified.  Also includes information
   on which signatures declare a field with a particular name (useful for desugaring
   with and for type inference; see {@link alloy.semantic.ExprTypeCheckVisitor}).
 */
public class ModuleInfo {
    /** name of the module for which this is a moduleinfo **/
    private QualifiedName _moduleName;
    
    /** Mapping of aliases to names of modules opened by the Module to which 
	this ModuleInfo corresponds **/
    private Map /**[QualifedName->QualifiedName]*/ _aliasesToModuleNames;

    /**
     * A set of BasicTypes in this module which must be made atomic 
     * because a closure operator is applied to them.
     **/
    private Set _closedTypes = Collections.EMPTY_SET;
    
    /**
     * A tree that stores how many times a signature is referenced in the declaration 
     * of fields
     */
    private SignatureReferenceCounter.CountTree _sigRefCountTree;

    /**
     * Maps unqualified {@link String} names to one or more
     * {@link Paragraph} paragraphs.  More than one paragraph
     * if two different modules have paragraph with same name,
     * one is opened from the other.
     * includes all paragraph names in OR directly
     * opened by this.module
     */
    private Map _nameToPara = new HashMap();

    /**
     * Maps {@link String} qualified names to exactly one
     * {@link Paragraph} paragraph
     * includes all paragraph names in OR directly
     * opened or used by this.module
     */
    private Map _qualNameToPara = new HashMap();

    /**
     * Maps {@link String} field names to ArrayLists of
     * {@link Signature} sigs that the field name may belong to
     * includes all field names in OR directly opened or used by this module.
     * used in
     * desugaring of "with" construct {@link ExprTypeCheckVisitor#visit(WithNode)}
     */
    private Map _fieldsToSigs = new HashMap();



    public ModuleInfo(Module module_) {
	_aliasesToModuleNames = module_.getAliasMappings();
	_moduleName = module_.getName();
    }

    public QualifiedName getModuleName() { return _moduleName; }

    /**
     * Sets the closed types of this module
     * @param closedTypes_ set of BasicTypes that are closed in this module
     **/
    public void setClosedTypes(Set closedTypes_) {
	_closedTypes = Collections.unmodifiableSet(closedTypes_);
    }

    /**
     * Gets the closed types of this module
     * @return an unmodifiable view of the set of closed types in this module
     **/
    public Set getClosedTypes() {
	return _closedTypes;
    }
    
    /**
     * Sets the signature reference count tree of this module
     * 
     * @param ct
     */
    public void setSigRefCountTree(SignatureReferenceCounter.CountTree ct) {
        _sigRefCountTree = ct;
    }
    
    /**
     * gets the signature reference count tree of this module
     * @return
     */
    public SignatureReferenceCounter.CountTree getSigRefCountTree() {
        return _sigRefCountTree;
    }

    /**
     * adds a paragraph that is used by this.module
     * @param name_, qualified name of the paragraph to add
     * @param paragraph_, the paragraph to add
     * @throw AlreadyMappedException if name_ already mapped to a paragraph
     */
    public void addUsedParagraph(QualifiedName name_, Paragraph paragraph_) throws AlreadyMappedException {
        Dbg.chk(name_ != null, "attempt to add null name");
        Dbg.chk(paragraph_ != null, "attempt to add null paragraph");
        String nameString = name_.nodeString();
        if (_qualNameToPara.containsKey(nameString)) {
            throw new AlreadyMappedException();
        } else {
            _qualNameToPara.put(nameString, paragraph_);
        }

	//add fields for signatures, only needed in uses method since everything opened is used.
	if (paragraph_ instanceof Signature){
            addFieldSigMappings((Signature)paragraph_);
	}
    }

    public Collection getParagraphs() {
	return _qualNameToPara.values();
    }

    /**
     * adds a paragraph that is opened by this.module
     * adds paragraph to both qualified and unqualified
     * name to paragraph mappings
     * @param name_, qualified name of the paragraph to add
     * @param paragraph_, the paragraph to add
     * @throw AlreadyMappedException if name_ already mapped to a paragraph
     */
    public void addOpenedParagraph(QualifiedName name_, Paragraph paragraph_) throws AlreadyMappedException {
        addUsedParagraph(name_, paragraph_);
        // add unqualified name to _nameToPara mapping
        // check if name is already mapped
        String unqualName = name_.getId().nodeString();
        if (_nameToPara.containsKey(unqualName)) {
            // check if name mapped to a list already
            Object mappedTo = _nameToPara.get(unqualName);
            if (mappedTo instanceof List) {
                // add the type to the list
                ((List)mappedTo).add(paragraph_);
            } else {
                // create a list holding mappedTo
                // and paragraph_, and set the table to map
                // unqualName to the ArrayList
                List mappedParas = new ArrayList();
                mappedParas.add(mappedTo);
                mappedParas.add(paragraph_);
                _nameToPara.put(unqualName, mappedParas);
            }
        } else {
            // add a mapping from unqualName to paragraph_
            _nameToPara.put(unqualName, paragraph_);
        }
    }

    /**
     * add mappings for the fields of a signature to this
     * @param sig_ the signature
     */
    public void addFieldSigMappings(Signature sig_) {
        Iterator decls = (sig_).getDecls().getDeclIter();
        Decl decl;

        while(decls.hasNext()){
            decl = (Decl)decls.next();
            if (!decl.isEmpty()) {
                Iterator varIter = decl.getVariables().getVariableIter();
                while (varIter.hasNext()) {
                    Variable curVar = (Variable)varIter.next();
                    String varName = curVar.getId().nodeString();
                    addFieldSigMapping(varName, sig_);
                }
            }
        }
    }

    /**
     * had to make this public for HACKISH atomization purposes (info about the 
     * mangled fields).  If there's a better solution let me know
     * 
     * adds a field to sig mapping to this
     * @param field_ field to be mapped
     * @param sig_ sig to be mapped to
     */
    public void addFieldSigMapping(String field_, Signature sig_) {
        Dbg.chk(field_ != null, "attempt to add null field");
        Dbg.chk(sig_ != null, "attempt to add null signature");
        List mappedSigs;
        if (_fieldsToSigs.containsKey(field_)) { // see if field already mapped
            mappedSigs = (List)_fieldsToSigs.get(field_);
            // this is actually not a problem
            //Dbg.chk(!mappedSigs.contains(sig_), "attempt to map field: " + field_ + " to sig: " + sig_.orignodeString() + " more than once");
            // add new mapping
            mappedSigs.add(sig_);
        } else {
            // create new ArrayList containing sig_ and
            // map field_ to it
            mappedSigs = new ArrayList();
            mappedSigs.add(sig_);
            _fieldsToSigs.put(field_, mappedSigs);
        }
    }

    /**
     * gets set of sigs that contain a certain field
     * @param field_ the relevant field
     * @return a {@link List} of sigs
     * @throw NoSigsException no sigs have such a field
     */
    public List getSigsForField(String field_) throws NoSigsException {
        List sigs = (List)_fieldsToSigs.get(field_);
        if (sigs == null) throw new NoSigsException();
        return new ArrayList(sigs);
    }


    /**
     * returns the paragraph that is associated with name_ in this scope
     * @param name_, unqualified name of the paragraph to get
     * @return the {@link Paragraph}
     * @throw MultipleMappingsException requested name maps to multiple paragraphs
     * @throw NoParagraphException name_ maps to no paragraph
     */
    public Paragraph getParagraphUnqual(QualifiedName name_) throws MultipleMappingsException, NoParagraphException {
        Dbg.chk(name_.hasEmptyPath(), "attempt to use qualified name in unqualified lookup");
        Object mappedTo = _nameToPara.get(name_.nodeString());
        if (mappedTo instanceof List) {
            throw new MultipleMappingsException((List)mappedTo);
        } else {
            if (mappedTo == null) {
                throw new NoParagraphException();
            }
        }
        return (Paragraph)mappedTo;
    }

    /** 
     * If the path of name_ contains any aliases, they are
     * substituted by their real names.
     * Otherwise, returns name_.  Assumes that name_ is qualified.
     **/
    private QualifiedName getName(QualifiedName name_) {
	Ids pathIds = name_.getPath().getPackages();
	int pathSize = pathIds.numChildren();
	
	ModuleId moduleId = (ModuleId) pathIds.childAt(pathSize - 1);
	
	QualifiedName aliasName = new QualifiedName(moduleId, new Path());
	QualifiedName parentName = (QualifiedName) _aliasesToModuleNames.get(aliasName);

	if (parentName == null) { // not an alias, substitute all type params that are aliases
	    QualifiedNames typeParams = new QualifiedNames();
	    
	    for(Iterator iter = moduleId.getTypeParams().getQualifiedNameIter(); 
		iter.hasNext();) {
		typeParams.addQualifiedName(getName((QualifiedName) iter.next()));
	    }

	    // construct a new name for the parent module of name_, which
	    // contains no aliases in its type parameters
	    moduleId = new ModuleId(moduleId.getLocation(),
				    moduleId.unparameterizedNodeString(),
				    typeParams);

	    // construct the path for the parent module
	    Ids parentPathIds = new Ids();
	    for(Iterator iter = pathIds.getIdIter(); parentPathIds.numChildren() < pathSize-1;) {
		parentPathIds.addId((Id)iter.next());
	    }
	    
	    parentName = new QualifiedName(moduleId, new Path(parentPathIds));
	    
	    
	} 
	return new QualifiedName(name_.getLocation(),
				 name_.getId(),
				 parentName);
	
    }


    /**
     * returns the paragraph that is associated with name_ in this scope
     * @param name_, qualified name of the paragraph to get
     * @return the {@link Paragraph}
     * @throw NoParagraphException name_ maps to no paragraph
     */
    public Paragraph getParagraph(QualifiedName name_) throws NoParagraphException {
	Dbg.chk(!name_.hasEmptyPath(), "attempt to use unqualified name in qualified lookup");
	Object mappedTo = _qualNameToPara.get(getName(name_).nodeString());
        if (mappedTo == null) throw new NoParagraphException();
        return (Paragraph)mappedTo;
    }

    /**
     * returns the paragraph that is associated with name_ in this scope
     * @param name_, String unqualified name of the paragraph to get
     * @return the {@link Paragraph}
     * @throw MultipleMappingsException requested name maps to multiple paragraphs
     * @throw NoParagraphException name_ maps to no paragraph
     */
    public Paragraph getParagraph(String name_) throws MultipleMappingsException, NoParagraphException {
        Object mappedTo = _nameToPara.get(name_);
        if (mappedTo instanceof List) {
            throw new MultipleMappingsException((List)mappedTo);
        } else {
            if (mappedTo == null) {
                throw new NoParagraphException();
            }
        }
        return (Paragraph)mappedTo;
    }

    private static void _err(String actionDesc_, String paraDesc_, Node node_) {
	if (actionDesc_ != null)
	    Dbg.user(new Msg("attempt to " + actionDesc_ + " " + paraDesc_, node_));
	//throw new RuntimeException();
    }

    /**
       Get a signature paragraph with a certain name.  If the signature with the given name
       does not exist or multiple paragraphs share the name, returns null
       @param name_ the name of the desired signature, can be qualified or unqualified
       @return the signature or null, if an error occurs
    */
    
    public Signature getSignature(QualifiedName name_, String actionDesc_) {
        
	Signature ret = null;
       
	try {
	    Paragraph para;
	    if (name_.hasEmptyPath()) { // unqualified name
		para = getParagraphUnqual(name_);
	    } else { // qualified name
		para = getParagraph(name_);
	    }
	    if (para instanceof Signature) {
		ret = (Signature) para;
	    } else {
		_err(actionDesc_, "a non-signature: "+name_.nodeString(), name_);
	    }
	} catch (ModuleInfo.MultipleMappingsException mme) {
	    Dbg.user(new Msg(mme.mappingsString(), name_));
	} catch (ModuleInfo.NoParagraphException npe) {
	    
	    if (actionDesc_ != null)
		_err(actionDesc_, "a non-existent signature: "+name_.nodeString(), name_);
	 
	}

	return ret;
	
        
    } 

    /**
     * Get the built-in Signature Int that is visible from this ModuleInfo;
     * returns null if Int is not visible from this ModuleInfo
     * @return the signature or null
     **/
    public Signature getInt() {
	return getSignature(new QualifiedName(new Id("Int"), new Path()), null);
    }
    
    /**
     * Get the built-in Signature univ that is visible from this ModuleInfo
     * @return the signature
     **/
    public Signature getUniv() {
	return getSignature(new QualifiedName(new Id("univ"), new Path()), null);
    }

    /**
       Get a function paragraph with a certain name.  If the function does not exist, or if
       multiple paragraphs share the name, creates an error message using {@link alloy.util.Dbg#user}.
       @param name_ the name of the desired function, can be qualified or unqualified
       @param actionDesc_ the action for which the function is needed.  used in error messages.
       @return the function, or <code>null</code> if an error occurs
    */
    public InvocablePara getInvocable(QualifiedName name_, String actionDesc_) {
        InvocablePara ret = null;
        Paragraph para;
        try {
            if (name_.hasEmptyPath()) { // unqualified name
                para = getParagraphUnqual(name_);
            } else { // qualified name
                para = getParagraph(name_);
            }
            if (para instanceof InvocablePara) {
                ret = (InvocablePara) para;
            } else {
                _err(actionDesc_,"a non-function", name_);
            }
        } catch (MultipleMappingsException mme) {
            Dbg.user(new Msg(mme.mappingsString(), name_));
        } catch (ModuleInfo.NoParagraphException npe) {
            _err(actionDesc_,"a non-existent function", name_);
        }
        return ret;
    }

    /**
       Get a assertion paragraph with a certain name.  If the assertion does not exist, or if
       multiple paragraphs share the name, creates an error message using {@link alloy.util.Dbg#user}.
       @param name_ the name of the desired assertion, can be qualified or unqualified
       @param actionDesc_ the action for which the assertion is needed.  used in error messages.
       @return the assertion, or <code>null</code> if an error occurs
    */
    public Assertion getAssertion(QualifiedName name_, String actionDesc_) {
        Assertion ret = null;
        Paragraph para;
        try {
            if (name_.hasEmptyPath()) { // unqualified name
                para = getParagraphUnqual(name_);
            } else { // qualified name
                para = getParagraph(name_);
            }
            if (para instanceof Assertion) {
                ret = (Assertion) para;
            } else {
                _err(actionDesc_,"a non-assertion", name_);
            }
        } catch (MultipleMappingsException mme) {
            Dbg.user(new Msg(mme.mappingsString(), name_));
        } catch (ModuleInfo.NoParagraphException npe) {
            _err(actionDesc_,"a non-existent assertion", name_);
        }
        return ret;
    }

    /**
       Get a fact paragraph with a certain name.  If the fact does not exist, or if
       multiple paragraphs share the name, creates an error message using {@link alloy.util.Dbg#user}.
       @param name_ the name of the desired fact, can be qualified or unqualified
       @param actionDesc_ the action for which the fact is needed.  used in error messages.
       @return the fact, or <code>null</code> if an error occurs
    */
    public Fact getFact(QualifiedName name_, String actionDesc_) {
        Fact ret = null;
        Paragraph para;
        try {
            if (name_.hasEmptyPath()) { // unqualified name
                para = getParagraphUnqual(name_);
            } else { // qualified name
                para = getParagraph(name_);
            }
            if (para instanceof Fact) {
                ret = (Fact) para;
            } else {
                _err(actionDesc_,"a non-fact", name_);
            }
        } catch (MultipleMappingsException mme) {
            Dbg.user(new Msg(mme.mappingsString(), name_));
        } catch (ModuleInfo.NoParagraphException npe) {
            _err(actionDesc_,"a non-existent fact", name_);
        }
        return ret;
    }

    public static class MultipleMappingsException extends Exception {

        /**
         * ArrayList holding all mappings for the name
         * can be a list of Types or Paragraphs
         */
        public List mappedTo;

        public MultipleMappingsException() {
            super();
        }

        public MultipleMappingsException(List mappedTo_) {
            mappedTo = mappedTo_;
        }

        public String mappingsString() {
            StringBuffer msg = new StringBuffer("reference to ambiguous unqualified name, could be ");
            Iterator possibleParas = mappedTo.iterator();
            while (possibleParas.hasNext()) {
                msg.append(((Paragraph)possibleParas.next()).getName());
                if (possibleParas.hasNext()) {
                    msg.append(" or ");
                }
            }
            return msg.toString();
        }

    }
    public class NoParagraphException extends Exception {}
    public class NoSigsException extends Exception {}
}


